Inference at * 1 
Iof proof for Lemma p-id-compose:

.....truecase..... NILNIL

1. A : Type
2. B : Type
3. f : A(B + Top)
4. x : A
5. can-apply(f;x)
  p-id()(do-apply(f;x)) = f(x) 

latex

 by (MoveToConcl (-1)) 
CollapseTHEN ((RepUR ``p-id can-apply do-apply`` ( 0)) 
CollapseTHEN (((
CGenConclAtAddr [1;1;1]) 
CollapseTHENA (Auto)) 
CollapseTHEN ((D (-2)) 
CollapseTHEN ((
CReduce 0) 
CollapseTHEN (Auto))))) 

latex

C.

Definitions	can-apply(f;x), p-id(), do-apply(f;x), f(a), Top, s = t, x:A. B(x), x:AB(x), left + right, True, b, P  Q, t  T, False
Lemmas	true wf, false wf